(set-logic QF_BV)
(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x4 () (_ BitVec 32))
(declare-fun x5 () (_ BitVec 32))
(declare-fun x6 () (_ BitVec 32))
(assert (let ((?v_21 (bvadd (bvmul (bvsub (_ bv0 32) (_ bv48 32)) x1) (_ bv0 32)))) (and true (not (= x6 (_ bv0 32))) true (= (_ bv0 32) ?v_21) true (= ?v_21 x4) (= x4 x0) (= x0 x5) (= x5 x3) (= x3 x2) (= x2 x6))))
(check-sat)
(exit)
